| Definitions | es-interface-history(es;X;e), t  T, s = t, x:A  B(x),  x:A. B(x),  b,  A, ES, Type, AbsInterface(A), E(X), ff, prior(X), e  X,  ,  , <a, b>, x:A  B(x), left + right, {x:A| B(x)} , type List, b, tt, E, let x,y = A in B(x;y), t.1, a:A fp B(a), strong-subtype(A;B), P   Q, Void,  x:A.B(x), Top, P  Q, P & Q, P Q, f(x)?z, p =b q, i <z j, i  z j, (i = j), x =a y, null(as), a < b, f(a), x f y, a < b, [d], eq_atom$n(x;y), q_le(r;s), q_less(a;b), qeq(r;s), a = b, a = b, deq-member(eq;x;L), e = e', p q, p  q, p  q,  , Unit, EState(T), Id,  , EqDecider(T), IdLnk, EOrderAxioms(E; pred?; info), kindcase(k; a.f(a); l,t.g(l;t) ), Knd, loc(e), kind(e), Msg(M),  , val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), r s, e < e', constant_function(f;A;B), SWellFounded(R(x;y)), pred!(e;e'),   x,y. t(x;y), S  T, suptype(S; T), first(e), pred(e), x.A(x), x. t(x), X(e), if b then t else f fi , pred(e), first(e), e loc e' ,  x:A. B(x), A c B, case b of inl(x) => s(x) | inr(y) => t(y), (e <loc e'), e(e1,e2].P(e), @e(x v), (last change to x before e), (e < e'), f g, loc(e), vartype(i;x), state@i, State(ds), State(ds), x dom(f), False, {T}, True,  T, P Q, as @ bs, es-le-before(es;e), mapfilter(f;P;L), concat(ll), [e, e'], inr x , inl x , ||as||, A B, Dec(P), b | a, a ~ b, a b, a <p b, a < b, xL. P(x), (xL.P(x)), r < s, q-rel(r;x), Outcome, (x l), l_disjoint(T;l1;l2), e c e', e<e'.P(e), ee'.P(e), e<e'. P(e), ee'.P(e), e[e1,e2).P(e), e[e1,e2).P(e), e[e1,e2].P(e), e[e1,e2].P(e), e(e1,e2].P(e), SqStable(P), a =!x:T. Q(x), InvFuns(A;B;f;g), Inj(A;B;f), IsEqFun(T;eq), Refl(T;x,y.E(x;y)), Sym(T;x,y.E(x;y)), Trans(T;x,y.E(x;y)), AntiSym(T;x,y.R(x;y)), Connex(T;x,y.R(x;y)), CoPrime(a,b), Ident(T;op;id), Assoc(T;op), Comm(T;op), Inverse(T;op;id;inv), BiLinear(T;pl;tm), IsBilinear(A;B;C;+a;+b;+c;f), IsAction(A;x;e;S;f), Dist1op2opLR(A;1op;2op), fun_thru_1op(A;B;opa;opb;f), FunThru2op(A;B;opa;opb;f), Cancel(T;S;op), monot(T;x,y.R(x;y);f), IsMonoid(T;op;id), IsGroup(T;op;id;inv), IsMonHom{M1,M2}(f), a b, IsIntegDom(r), IsPrimeIdeal(R;P), i  j , s ~ t, SQType(T), [car / cdr], [], A List , Atom$n, map(f;as), filter(P;l), before(e), es-ble{i:l}(es;e;e'), |g|, a < b, l[i], x(s), #$n, es-interface-sublist(X;z), rcv(l,tg), locl(a), Y |
| Lemmas | es-is-prior-interface, member-es-before, append-nil, es-interval-eq2, es-interface-sublist wf, es-interval-eq, es-locl transitivity2, es-prior-interface-val, es-locl transitivity1, es-pred-locl, all functionality wrt iff, implies functionality wrt iff, member-es-interval, iff wf, rev implies wf, select wf, filter is nil, length wf1, es-ble wf, es-before wf, filter append, es-locl-iff, es-interval-partition, es-le weakening eq, filter wf, map wf, mapfilter-append, concat append, es-interval wf2, es-loc wf, l member wf, subtype rel list, non neg length, cons one one, guard wf, length wf nat, es-interval wf, sq stable from decidable, decidable assert, le wf, false wf, btrue wf, bfalse wf, es-le-before-partition2, es-le-before wf, mapfilter wf, concat wf, append wf, es-le wf, es-first wf, es-pred wf, es-interface-val wf2, es-next, squash wf, true wf, es-E-interface-subtype rel, es-locl wf, es-causl wf, es-prior-interface-locl, es-interface-history wf, es-interface-val wf, ifthenelse wf, deq wf, EOrderAxioms wf, kind wf, Msg wf, nat wf, val-axiom wf, cless wf, qle wf, Knd wf, kindcase wf, IdLnk wf, constant function wf, loc wf, first wf, unit wf, pred! wf, strongwellfounded wf, rationals wf, Id wf, EState wf, event system wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, es-is-interface wf, es-prior-interface wf, es-interface wf, es-interface-subtype rel, top wf, member wf, es-E wf, es-E-interface wf, subtype rel wf, bool wf, bnot wf, not wf, assert wf |